<html>
<head><meta charset="utf-8"><title>MIR vs HAIR · wg-formal-methods · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/index.html">wg-formal-methods</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/MIR.20vs.20HAIR.html">MIR vs HAIR</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="213931532"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/MIR%20vs%20HAIR/near/213931532" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/MIR.20vs.20HAIR.html#213931532">(Oct 20 2020 at 14:59)</a>:</h4>
<p>Does anyone have experience / opinions on working from a higher-level IR than MIR for verification? We were recently talking about the tradeoffs of using MIR so I was wondering if anyone has toyed with something like HAIR</p>



<a name="213931717"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/MIR%20vs%20HAIR/near/213931717" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/MIR.20vs.20HAIR.html#213931717">(Oct 20 2020 at 15:00)</a>:</h4>
<p>does HAIR / HIR have _any_ stability guarantee? it seems like changes to MIR are carefully weighted and I don't know if that also applies to hair</p>



<a name="213938434"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/MIR%20vs%20HAIR/near/213938434" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/MIR.20vs.20HAIR.html#213938434">(Oct 20 2020 at 15:47)</a>:</h4>
<p>Do you need the borrow checker information? If yes, wouldn't it be a big problem to represent its CFG-based information on an AST?</p>



<a name="213984218"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/MIR%20vs%20HAIR/near/213984218" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/MIR.20vs.20HAIR.html#213984218">(Oct 20 2020 at 21:53)</a>:</h4>
<p>that's the BIG downside to non-mir approaches</p>



<a name="213984307"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/MIR%20vs%20HAIR/near/213984307" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/MIR.20vs.20HAIR.html#213984307">(Oct 20 2020 at 21:54)</a>:</h4>
<p>so far we don't need _lifetimes_ but borrow-aliveness</p>



<a name="213984318"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/MIR%20vs%20HAIR/near/213984318" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/MIR.20vs.20HAIR.html#213984318">(Oct 20 2020 at 21:54)</a>:</h4>
<p>still obviously a major downside</p>



<a name="214030451"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/MIR%20vs%20HAIR/near/214030451" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/MIR.20vs.20HAIR.html#214030451">(Oct 21 2020 at 10:02)</a>:</h4>
<p><span class="user-mention silent" data-user-id="312719">Xavier Denis</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/MIR.20vs.20HAIR/near/213984307">said</a>:</p>
<blockquote>
<p>so far we don't need _lifetimes_ but borrow-aliveness</p>
</blockquote>
<p>But borrow-aliveness information is computed by the borrow checker that works on MIR, so you would need somehow to pull this information back to HAIR. Am I missing something?</p>



<a name="214030475"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/MIR%20vs%20HAIR/near/214030475" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/MIR.20vs.20HAIR.html#214030475">(Oct 21 2020 at 10:03)</a>:</h4>
<p>you're completely right</p>



<a name="214030492"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/MIR%20vs%20HAIR/near/214030492" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/MIR.20vs.20HAIR.html#214030492">(Oct 21 2020 at 10:03)</a>:</h4>
<p>I just wanted to be clear about what information we're talking about</p>



<a name="214068875"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/MIR%20vs%20HAIR/near/214068875" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jubilee <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/MIR.20vs.20HAIR.html#214068875">(Oct 21 2020 at 15:39)</a>:</h4>
<p>I think MIR and HIR both enjoy relative stability, but ultimately they're still both implementation details of the compiler and as such subject to change without warning. The dilemma tho' is that they affect so many places <em>in the compiler</em> that they don't change very often.</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>